package org.cos.verifier.automata;

import java.util.Enumeration;
import java.util.Hashtable;
import java.util.Stack;
import java.util.Vector;

class TransformTable {
	//transitions[src_id] = {dst_id: [method ...] , ...}
	public Hashtable index =  null;
	
	
	public TransformTable(){
		this.index = new Hashtable();
	}
	
	public void add_transition(int src_id, int dst_id, Transition tran) {
		if ( ! index.containsKey(new Integer(src_id))) {
			index.put(new Integer(src_id), new Hashtable());
		} 
//		if ( ! index.containsKey(new Integer(dst_id))) {
//			index.put(new Integer(dst_id), new Hashtable());
//		}
		
		Hashtable transforms = (Hashtable) index.get(new Integer(src_id));
		Vector trans;
		if ( ! transforms.containsKey(new Integer(dst_id))) {
			trans = new Vector();
		} else {
			trans = (Vector) transforms.get(new Integer(dst_id));
		}
		trans.addElement(tran);
		transforms.put(new Integer(dst_id), trans);
		//DEBUG System.out.println("Add trans: "+ src_id+"->"+ dst_id+":" + tran.method);
		index.put(new Integer(src_id), transforms);
		
	}
	
    public Vector get_transitions(int src_id) {
    	Vector ret = new Vector();
		Hashtable transform = (Hashtable) index.get(new Integer(src_id));
		//DEBUG System.out.println(src_id + ": "+transform);
		
    	for (Enumeration e2 = transform.keys(); e2.hasMoreElements();){
    		Integer dst_id = (Integer) e2.nextElement();
    		Vector trans = (Vector) transform.get(dst_id);
    		for (Enumeration e3 = trans.elements(); e3.hasMoreElements();){
    			ret.addElement(new Pair(dst_id, e3.nextElement()));
    		}
    	}
    	return ret;
    }
       
}



public class Automata {

	public String name;
	// trans_table: {tran.dst_state_id: method ... }
	public TransformTable tranform_table;
	private Vector trans;
	public Hashtable state_set;
	public Vector final_state_set ;
	private Vector init_state ;
	public Vector init_var;
	
	public Automata(){
		this("");
	}
	
	public Automata(String name) {
		this.name = name;
		tranform_table = new TransformTable(); 
		trans = new Vector();
		state_set = new Hashtable();
		final_state_set = new Vector();
		init_state = new Vector();
		init_var = new Vector();
	}

	public boolean is_final(Integer id) {
		return final_state_set.contains(id);
	}
	public boolean is_init(Integer id) {
		return init_state.contains(id);
	}
	
	public Automata add_state(int src_id) {
		Integer id = new Integer(src_id);
		state_set.put(id, id);
		if ( ! tranform_table.index.containsKey(id)) {
			tranform_table.index.put(id, new Hashtable());
		} 
		return this;
	}

	
	public Automata set_final(int state_id) {
		if (! final_state_set.contains(new Integer(state_id)))
			final_state_set.addElement(new Integer(state_id));
		return this;
	}

	public Automata set_transition(int src_id, int dst_id,
			Transition tran) {
		tranform_table.add_transition(src_id, dst_id, tran);
		return this;

	}

	public Automata set_init(int state_id) {
		init_state.addElement(new Integer(state_id));
		return this;
	}
	
	// Added by ZXD on 2009.5.9
	public Automata add_var(String name, String type, Object init) {
		if (type != null && type.equals("SET")) {
			Hashtable set = new Hashtable();
			if (init != null) set.put(init, init);
			if (name != null) init_var.add(set);
		} else {
			init_var.add(init);
		}
		return this;
	}
	
	// Added by ZXD on 2009.5.10
	public Automata add_vars(Vector vars) {
		init_state.addAll(vars);
		return this;
	}
	
	public void print(){
		System.out.println("name: " + this.name);
		System.out.print("states: [");
		for (Enumeration enumobj = this.state_set.elements(); enumobj.hasMoreElements();) {
			Integer s = (Integer)enumobj.nextElement();
			System.out.print( s.intValue() + ",");
		}
		System.out.println("]");

		System.out.print("init states: ");
		for (Enumeration enumobj = init_state.elements(); enumobj.hasMoreElements();) {
			Integer fs = (Integer)enumobj.nextElement();
			System.out.print("[" + fs.intValue() + "]");
		}
		System.out.println();

		System.out.print("final states: ");
		for (Enumeration enumobj = final_state_set.elements(); enumobj.hasMoreElements();) {
			Integer fs = (Integer)enumobj.nextElement();
			System.out.print("[" + fs.intValue() + "]");
		}
		System.out.println();
		
		System.out.println("trans: ");
		for (Enumeration enumobj = this.state_set.elements(); enumobj.hasMoreElements();) {
			int src_id = ((Integer)enumobj.nextElement()).intValue();
			//DEBUG System.out.println(src_id);
			Vector trans_pair = this.tranform_table.get_transitions(src_id);

			for (Enumeration enum_tran = trans_pair.elements(); enum_tran.hasMoreElements();) {
				Pair p = (Pair)enum_tran.nextElement();

				Integer dst_id = (Integer) p.head;
				Transition tran = (Transition) p.tail;

				//System.out.println(methods.get(new Integer(tran.method_id)).toString());
				System.out.print("[" 
						+ src_id + "->" + dst_id + ":"+ tran.method + "]"); 
				
				for (Enumeration enum_cond = tran.conditions.elements(); enum_cond.hasMoreElements();) {
					Condition cond = (Condition)enum_cond.nextElement();
					System.out.print("{" + cond.target_id +":"+cond.type);
					for (Enumeration enum_set = cond.sets.elements(); enum_set.hasMoreElements();) {
						CondSet set = (CondSet) enum_set.nextElement();
						System.out.print("|" + set.relation + "<" +set.value_d + "," +set.value_u + ">");
					}
					System.out.print("}");
				}
				
				for (Enumeration enum_act = tran.actions.elements(); enum_act.hasMoreElements();) {
					Action act = (Action)enum_act.nextElement();
					System.out.print("[" + act.type + ":" + act.opt + ":" + act.value + "]");
				}
				System.out.println( );
			}
			
		}
		System.out.println();
		
	}
	
	
	public void print_dot(){
		System.out.println("digraph G_A_x_B { \nrankdir=LR;");
		for (Enumeration enumobj = this.state_set.elements(); enumobj.hasMoreElements();) {
			Integer s = (Integer)enumobj.nextElement();
			System.out.println("\""+ s.intValue() +"\" [shape=\"circle\"];");
		}
		
		for (Enumeration enumobj = this.state_set.elements(); enumobj.hasMoreElements();) {
			int src_id = ((Integer)enumobj.nextElement()).intValue();
			//DEBUG System.out.println(src_id);
			Vector trans_pair = this.tranform_table.get_transitions(src_id);

			for (Enumeration enum_tran = trans_pair.elements(); enum_tran.hasMoreElements();) {
				Pair p = (Pair)enum_tran.nextElement();

				Integer dst_id = (Integer) p.head;
				Transition tran = (Transition) p.tail;
				//System.out.println(methods.get(new Integer(tran.method_id)).toString());
				System.out.println("\"" 
						+ src_id + "\"->\"" + dst_id + "\" [label=\""+ tran.method + "\"];"); 
			}
			
		}
		System.out.println("}");
	}
	
	private void merge_states(AutomataBuilder ab, Automata am, Hashtable temp_map){
		Integer temp_map_counter = new Integer(0);

		for (Enumeration enum_my_id = state_set.elements(); enum_my_id.hasMoreElements();){
			Integer my_id = (Integer)enum_my_id.nextElement();
			for (Enumeration enum_your_id = am.state_set.elements(); enum_your_id.hasMoreElements();){
				Integer your_id = (Integer)enum_your_id.nextElement();

				Integer new_child_id = temp_map_counter;
				
				//Modified by ZXD on 2009.5.8
				boolean is_init = this.is_init(my_id) && am.is_init(your_id);
				boolean is_final = am.is_final(your_id);
				
				ab.set_state(new_child_id.intValue(), is_init, is_final);
				temp_map.put( new Pair(my_id, your_id), new_child_id);

				temp_map_counter = new Integer(temp_map_counter.intValue() +1);
			}
		}
	}
	
	private void merge_transitions(AutomataBuilder ab, Automata am, Hashtable temp_map, int var_off){
		for (Enumeration enum_print_k1 = this.state_set.elements(); enum_print_k1.hasMoreElements();) {
			Integer my_state_id = (Integer) enum_print_k1.nextElement();
			Vector my_transforms = this.tranform_table.get_transitions(my_state_id.intValue());
			
			for (Enumeration enum_print_k2 = am.state_set.elements(); enum_print_k2.hasMoreElements();) {
				Integer your_state_id = (Integer) enum_print_k2.nextElement();
				Vector your_transforms = am.tranform_table.get_transitions(your_state_id.intValue());
				 
				for (Enumeration enum_my_transforms = my_transforms.elements(); enum_my_transforms.hasMoreElements();){
					Pair my_tran_p = (Pair) enum_my_transforms.nextElement();
					Integer my_dst_id = (Integer) my_tran_p.head;
					Transition my_tran = (Transition) my_tran_p.tail;
					Method my_method = (Method) my_tran.method;
					Vector my_conds = (Vector) my_tran.conditions;
					Vector my_acts = (Vector) my_tran.actions;

					boolean remainFlag = true;
					
					for (Enumeration enum_your_transforms = your_transforms.elements(); enum_your_transforms.hasMoreElements();){
						Pair your_tran_p = (Pair) enum_your_transforms.nextElement();
						Integer your_dst_id = (Integer) your_tran_p.head;
						Transition your_tran = (Transition) your_tran_p.tail;
						Method your_method = (Method) your_tran.method;
						Vector your_conds = (Vector) your_tran.conditions;
						Vector your_acts = (Vector) your_tran.actions;
						
						if (my_method.cmp_method(your_method)) { //Compare method
							boolean satisFlag = true;
							for (Enumeration my_cond_enum = my_conds.elements(); my_cond_enum.hasMoreElements();){
								Condition my_cond = (Condition) my_cond_enum.nextElement();
								for (Enumeration your_cond_enum = your_conds.elements(); your_cond_enum.hasMoreElements();){
									Condition your_cond = (Condition) your_cond_enum.nextElement();
									Pair pair = my_cond.intersect(your_cond);
									if (pair != null) {
										Condition inter = (Condition) pair.head;
										if (inter == null) {
											satisFlag = false;
											break;
										}
									}
								}
								if (!satisFlag) break;
							}
							if (satisFlag) {
								Integer src_id = (Integer) temp_map.get(new Pair(my_state_id, your_state_id));
								Integer dst_id = (Integer) temp_map.get(new Pair(my_dst_id, your_dst_id));
								
								ab.build_transition(src_id.intValue(), dst_id.intValue(), my_method,
										 merge_conditions(my_conds, your_conds, var_off),
										 merge_actions(my_acts, your_acts, var_off));
								//DEBUG System.out.println("New Tran:" + src_id + "->"+dst_id + ":"+ my_method);
								remainFlag = false;
							}
						}
					}
					if (remainFlag) {
						Integer src_id = (Integer) temp_map.get(new Pair(my_state_id, your_state_id));
						Integer dst_id = (Integer) temp_map.get(new Pair(my_dst_id, your_state_id));
						
						//Modified by ZXD on 2009.5.8
						ab.build_transition(src_id.intValue(), dst_id.intValue(), my_method, my_conds, my_acts);
						//DEBUG System.out.println("New Tran:" + src_id + "->"+dst_id + ":"+ my_method);
					}
				}
			}
		}
	}

	// Modified by ZXD on 2009.5.8
	private Vector merge_conditions(Vector my, Vector your, int var_off){
		Vector ret = new Vector();
		ret.addAll(my);
		ret.addAll(your);
		for (int i = my.size(); i < ret.size(); i++) {
			Condition condition = (Condition) ret.get(i);
			if (condition.type.equals("VARIABLE"))
				condition.target_id += var_off; 
		}
//		for (Enumeration enum_my = my.elements(); enum_my.hasMoreElements();){
//			Condition my_cond= (Condition) enum_my.nextElement();
//			for (Enumeration enum_your = your.elements(); enum_your.hasMoreElements();){
//				Condition your_cond = (Condition) enum_your.nextElement();
//				if (my_cond.type.equalsIgnoreCase("PARAMETER")) {
//					
//				} else { //VARS
//					//TODO 
//				}
//			}
//		}
		return ret;
	}
	
	// Modified by ZXD on 2009.5.8
	private Vector merge_actions(Vector my, Vector your, int var_off){
		Vector ret = new Vector();
		ret.addAll(my);
		ret.addAll(your);
		for (int i = my.size(); i < ret.size(); i++) {
			Action action = (Action) ret.get(i);
			if (action.type.equals("VARIABLE"))
				action.target_id += var_off; 
		}
//		for (Enumeration enum_my = my.elements(); enum_my.hasMoreElements();){
//			ret.addElement(enum_my.nextElement());
//			for (Enumeration enum_your = your.elements(); enum_your.hasMoreElements();){
//				ret.addElement(enum_your.nextElement());
//				//TODO
//			}
//		}
		return ret;
	}
	
	private int merge_variables(AutomataBuilder ab, Automata am) {
		ab.build_var(this.init_var);
		ab.build_var(am.init_var);
		return this.init_var.size();
	}
	
	public Automata merge(Automata am) {
		AutomataBuilder ab = new AutomataBuilder();
		Hashtable temp_map = new Hashtable();
		
		//merge variables
		int var_off = merge_variables(ab, am);
		
		//merge states
		merge_states(ab, am, temp_map);
		
		//test print states
//		for (Enumeration enum_print_k = temp_map.keys(); enum_print_k.hasMoreElements();){
//			Pair p = (Pair) enum_print_k.nextElement();
//			Integer new_id = (Integer) temp_map.get(p);
//			Integer my_id = (Integer) p.head;
//			Integer your_id = (Integer) p.tail;
//			System.out.println("("+  my_id + ", " + your_id + "->" + new_id +" )");
//		}

		//merge transitions
		merge_transitions(ab, am, temp_map, var_off);

		
		
		return ab.get_automata();
	}
	
	// Modified by ZXD on 2009.5.9
	public boolean check(){
		// Store visited states.
		Hashtable visitedStates = new Hashtable();
		// State ID queue.
		Vector q = new Vector();
		// Stack queue.
		Vector stackQueue = new Vector();
		// Variables queue.
		Vector varsQueue = new Vector();
		// Put the initial state into queue.
		for (Enumeration enum_is = init_state.elements(); enum_is.hasMoreElements();) {
			Integer state_start = (Integer) enum_is.nextElement();
			q.addElement(state_start);
			stackQueue.add(new Stack());
			varsQueue.add(init_var);
		}
		// BFS!
		while (! q.isEmpty()) {
			Integer crr_state = (Integer) q.firstElement();
			Stack crr_stack = (Stack) stackQueue.firstElement();
			Vector crr_var = (Vector) varsQueue.firstElement();
			
			q.removeElementAt(0);
			stackQueue.removeElementAt(0);
			varsQueue.removeElementAt(0);
			
			Pair stateInfo = new Pair(crr_state, crr_stack.empty() ? null : crr_stack.peek());
			
			if (!visitedStates.containsKey(stateInfo)) {
				
				visitedStates.put(stateInfo, "1");
				
				if (final_state_set.contains(crr_state)) {
					return true;
				}
				
				Vector nexts = tranform_table.get_transitions(crr_state.intValue());
				for (Enumeration enum_next = nexts.elements(); enum_next.hasMoreElements();){
					Pair next_p = (Pair) enum_next.nextElement();
					
					Integer next_state = (Integer) next_p.head;
					Transition tran = (Transition) next_p.tail;
					Method method = (Method) tran.method;
					Vector conds = (Vector) tran.conditions;
					Vector acts = (Vector) tran.actions;
				

				
					boolean satisFlag = true;
					
					for (Enumeration enum_cond = conds.elements(); enum_cond.hasMoreElements();){
							Condition cond = (Condition) enum_cond.nextElement();
						if (cond.type.equals("STACK")) {
							if (crr_stack.isEmpty() || !cond.satisfy(crr_stack.peek())) {
								satisFlag = false;
								break;
							}
						}else if (cond.type.equals("VARIABLE")) {
							
						}
					}
					
					if (satisFlag) {
						
						Stack newStack = new Stack();
						Vector newVars = new Vector();
						
						newStack.addAll(crr_stack);
						newVars.addAll(crr_var);
						
						for (Enumeration enum_act = acts.elements(); enum_act.hasMoreElements();){
							Action act = (Action) enum_act.nextElement();
							if (act.type.equals("STACK")) {
								if (act.opt.equals("POP")) {
									newStack.pop();
								} else if (act.opt.equals("PUSH")) {
									newStack.push(act.value);
								}
							} else if (act.type.equals("VARIABLE")) {
								if (act.opt.equals("ASSIGN")) {
									
								}
							}
						}
						
						q.addElement(next_state);
						stackQueue.add(newStack);
						varsQueue.add(newVars);
					}
				}
			}
		}
		return false;
	}
	
}
